FDL - Nuprl Lemma : mu-bound-property+

Nuprl Lemma : mu-bound-property+

b:

, f:({0..b

}

).
(

n:{0..b

}. (

(f(n))))

{mu(f)

{0..b

} & (

(f(mu(f)))) & (

i:{0..b

}. (i < mu(f))

(

(

(f(i)))))}

Definitions x:A. B(x), P Q, x:A. B(x), t T, {T}, P & Q, ,

Lemmas mu-bound-property, int seg wf, assert wf, bool wf, nat wf, mu-bound